FDL - Step of Proof: assert_functionality_wrt

Step of Proof: assert_functionality_wrt_bimplies

Inference at *
Iof proof for Lemma assert functionality wrt bimplies:

u,v:

. (

v))

{(

(

v)}

by ((Unfold `guard` 0)

CollapseTHEN (((((((RepeatMFor 2 (D 0))

CollapseTHENM (BoolEval))

)

CoCollapseTHENM (AbReduce 0))

)

CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n

C),(first_nat 3:n)) (first_tok :t) inil_term)))

))

Definitions True, t T, tt, ff, if b then t else f fi , b, p q, {T}, p q, b, P Q, x:A. B(x), False, Unit, , ,

Lemmas bool wf, false wf, true wf

Definitions	True, t T, tt, ff, if b then t else f fi , b, p q, {T}, p q, b, P Q, x:A. B(x), False, Unit, , ,
Lemmas	bool wf, false wf, true wf